d-comp-partial-world(D; v; sched; dec; discrete; t)
== d-partial-world(D;CV(d-comp(D; v; sched; dec; discrete));t;i.if (t = 0)
== then x.M(i).init(x)?v(i,x)
== else (CV(d-comp(D; v; sched; dec; discrete))((t - 1),i)).1
== fi ;discrete) 

latex

---

clarification:

d-comp-partial-world(D; v; sched; dec; discrete; t)
== d-partial-world(D;CV(d-comp(D; v; sched; dec; discrete));t;i.if (t = 0)
== then x.d-m(D; i).init(x)?v(i,x)
== else (CV(d-comp(D; v; sched; dec; discrete))((t - 1),i)).1
== fi ;discrete) 

latex

Definitions

d-partial-world(D;f;t';s;d), if b then t else f fi , (i = j), x.A(x), M.init(x)?v, M(i), t.1, f(a), CV(F), d-comp(D; v; sched; dec; d), n - m, #$n